World
== T:(IdIdType)
==  (TA:(IdIdType)
==  M:(IdLnkIdType)
==  s:(i:Id(x:IdT(i,x)))
==  a:(i:IdAction(w-action-dec(TA;M;i)))
==  m:(i:Id({m:Msg(M)| source(mlnk(m)) = i}  List))
==  :(i:Idw-automaton(T(i);TA(i);M))
==  (discrete:(IdId)
==  Top)) 

latex

---

clarification:

world{i:l}
== T:(IdIdType{i})
==  (TA:(IdIdType{i})
==  M:(IdLnkIdType{i})
==  s:(i:Id(x:IdT(i,x)))
==  a:(i:IdAction(w-action-dec(TA;M;i)))
==  m:(i:Id({m:Msg(M)| source(mlnk(m)) = i  Id}  List))
==  :(i:Idw-automaton(T(i);TA(i);M))
==  (discrete:(IdId)
==  Top)) 

latex

Definitions	IdLnk, Type, , Action(dec), w-action-dec(TA;M;i), , type List, {x:A| B(x)} , Msg(M), s = t, source(l), mlnk(m), w-automaton(T;TA;M), f(a), x:A  B(x), x:AB(x), Id, , Top
FDL editor aliases	world